This paper reviewed some prevalent trends in this domain in recent years, then proposed a software model checking scenario, which was based on hierarchical unit partition and heuristic search. It has three phases, which are preprocess, unit partition and state space search. There is on-the-fly method in this scenario to improve the performance of model checking. Experiments prove that this model checking scenario works well on solving state explosion problem.